\chapter{Diseño e Implementación}
\section{Introducción}
Comenzamos detallando la estructura y el diseño que fue punto de partida para la construcción de \emph{FLWA}. Luego enumeramos las diferentes actividades realizadas en el marco de desarrollo de esta herramienta.\\\newline
La implementación toma dos partes principales o fundamentales, por un lado, la recolección de los datos a partir de un modelo \emph{YAWL} y la representación de esos datos gráficamente en un Canvas y por el otro la posibilidad de la definición de fluentes y propiedades, y en caso de éstas últimas la posibilidad de instanciarlas por medio de templates. Por último el análisis y validación de las restricciones definidas para posteriormente dar a conocer los resultados gráficamente.\\
Además en este capítulo se describirá fundamentos de codificación que fueron realizados para la elaboración de la herramienta.

\section{Diseño}
La figura 5.1 muestra el diseño arquitectónico del proceso de verificación de propiedades sobre un modelo de workflow por medio de \emph{FLWA}.\\
El proceso comienza con un modelo de workflow que se describe mediante el uso de la herramienta de modelado de workflow \emph{YAWL}.
\emph{FLWA} toma como entrada un modelo de workflow y ayuda a que el usuario fácilmente y de una manera gráfica, especifique y verifique las propiedades de este tipo de modelo. El proceso de verificación es manejado por el model checker \emph{LTSA} , por medio de una traducción del modelo y las propiedades de un sistema de transición estado etiquetado (LTS). De esta manera se podrá expresar las propiedades para los modelos de \emph{YAWL} que se ha deseado analizar, de manera declarativa usando la lógica \emph{FLTL}, que se detalló en el capítulo 2.\\
Esta herramienta posee dos módulos principales desarrolladas de manera independiente, el compilador ``YAWL2FSP'' que
codificar un modelo de workflow \emph{YAWL} en un \textit{FPS} y el entorno gráfico ``FLYAnlyser'' , que es responsable de facilitar a los usuarios el análisis y especificación de las propiedades, además, es el módulo encargado de la integración y comunicación de los componentes \emph{YAWL2FSP} y \emph{LTSA}.

\begin{figure}[htp] \centering{
\includegraphics[scale=0.35]{graphs/design.pdf}}
\caption{Diseño de \emph{FLWA}}
\end{figure}

Para la creación de \emph{FLWA} se utilizó el lenguaje JAVA, debido a la experiencia obtenida a lo largo del cursado y de las características que éste ofrece para la creación de una herramienta de estas características. Por otra parte, este lenguaje toma protagonismo dado que todas las herramientas las cuales \emph{FLWA} hace uso como \emph{YAWL}, \emph{LTSA}, y \emph{yawl2fsp} fueron creadas también en este lenguaje.
Debido a que la comunicación entre algunos de estos componentes se realiza por medio de archivos en el lenguaje interpretado XML. Se decidió utilizar los servicios que ofrece DOM Parser, en su implementan en JAVA aprovechando el lenguaje elegido.\\

\section{Estructura del Proyecto}
Aquí se da una vista de la composición de cada uno de los paquetes que conforman la herramienta desarrollada. La organización que revisten los módulos es producto de la utilización de diferentes herramientas que utiliza \textit{FLWA} para cumplir sus objetivos.\\\newline

\begin{figure}[htp] \centering{
\includegraphics[scale=0.6]{graphs/architecture.pdf}}
\caption{Arquitectura de \emph{FLWA}}
\end{figure}


En principio, \emph{FLWA} posee un módulo centralizado el cual controla todas las operaciones que ocurren en ella. Este módulo es el encargado de los procesos que debe realizar \emph{FLWA} pero también es el encargado de los procesos que se encargan de la comunicación con \emph{yawl2fsp} y \emph{LTSA}. Como \emph{FLWA} es una herramienta que cuenta con interfaz gráfica, cada una de éstas tiene su propio controlador el cual permite la integración de lo que ocurre visualmente con la información que se tiene temporalmente almacenada. Por otra parte, este módulo control es manejado por el controlador principal. \\
Para los casos de la comunicación con las otras herramientas, cada caso es particular. Para el caso con \emph{yawl2fsp} la comunicación está dada de dos formas; la primera de ella sucede cuando se desea obtener la especificación \textit{FSP}, por ende su uso está dado como aplicación externa, es decir, se ejecuta la aplicación \textit{yawl2fsp.jar} mediante linea de comandos. El otro uso de esta aplicación se da cuando se requiere los nombres utilizados en la especificación para la traducción de las propiedades y fluentes definidos a su correcta nomenclatura. En este caso \textit{yawl2fsp.jar} se utiliza como librería, ya que éste permite los servicios para realizar dicha traducción.\\
Por otro parte, \emph{LTSA} es una aplicación que no se puede ejecutar de manera interna, por lo que se solicito el código fuente a sus desarrolladores\cite{ltsaSource} para la comunicación con \emph{FLWA}. En consecuencia a esto, \emph{LTSA} se encuentra modificada y adaptada como un módulo adicional de \emph{FLWA}.

\section{Representación de modelos YAWL}

\subsection{Introducción}
El objetivo de esta sección consiste en mostrar el detalle de todos los pasos que fueron necesarios para la representación de los modelos generados por \emph{YAWL}. Por un lado se detallará el diseño del motor desarrollado para la recolección de la información que permite la visualización de los modelos y por el otro el módulo encargado de la presentación final de esta información en diagramas visuales.

\subsection{Motor XML}
Como se mencionó anteriormente, el editor de \emph{YAWL} genera los modelos en un archivo con formato \textit{xml}. Este archivo contiene información entre la que se podrá mencionar, el nombre del modelo \emph{YAWL}, las tareas que involucran en él, los estados o condiciones, información sobre las compuertas JOIN y SPLIT, etc. Por otra parte, contiene información de las relaciones entre cada uno de los elementos, como así también de los estados de INPUT y OUTPUT del modelo. Este archivo, adicionalmente incluye información gráfica, que involucra, posiciones dentro del plano de coordenadas $x$ e $y$ de todos los elementos del modelo, puntos de origen y destino de las relaciones representadas como flechas y los nombres de las tareas o condiciones. Por último el \textit{archivo.yawl} contiene también datos necesarios sobre las tareas compuestas como información de subredes o submodelos y de las regiones de cancelación de los mismos. \\
El Motor determina toda esta información respecto del los elementos como también información referente a los gráficos para posteriormente almacenarlos en diferentes estructuras, generalmente en listas enlazadas\footnote{LinkedList: Clase de JAVA utilizada para el almacenamiento de distintos elementos.}. Luego se define una estructura Diagram para almacenar toda la información referida al modelo y los fluentes definidos sobre él.\\
Las tareas compuestas como se mencionó anteriormente poseen información de submodelos, cada submodelo se almacena en un nuevo objeto Diagram que cual tendrá sus propias tareas o actividades, condiciones, posiciones compuertas, regiones de cancelación, etc.\\ Ademas podrá almacenar información sobre los fluentes que se definan sobre él. Estos diferentes diagramas se almacenan en una lista de manera de poder acceder fácilmente a ellos.

\subsection{DOM Parser}
Para extraer la información que contiene el documento \emph{YAWL} cuya información está definida sobre formato XML, se podría escribir código para analizar el contenido del archivo, puesto que no deja de ser un archivo de texto. Sin embargo, esta solución no es muy aconsejable y desaprovecharía una de las ventajas de XML el ser una forma estructurada de representar datos ya que éste cuenta con todos los tags que representan la forma y la información de cada objeto, además del uso del tiempo en el análisis del texto.\\
La mejor forma de recuperar información de archivos XML es utilizar un parser de XML, que sea compatible con el modelo de objeto de documento (DOM) de XML. DOM define un conjunto estándar de comandos que los parsers devuelven para facilitar el acceso al contenido de los documentos XML desde sus programas. Un analizador de XML compatible con DOM toma los datos de un documento XML y los expone mediante un conjunto de objetos lo cual hace mas rápida y eficiente su utilización.\\

DOM para XML es un modelo de objetos estándar (propuesto por el W3C) que muestra el contenido de un documento XML, en este caso el contenido del modelo \emph{YAWL}. La Especificación del Modelo de Objeto de documento (DOM) del W3C define actualmente lo que debería mostrar un DOM como propiedades, métodos y eventos. Este motor XML fue desarrollado en \textit{JAVA} aprovechando el uso de objetos y los conocimientos previos durante la carrera.
Contiene métodos de abstracción para la detección de la tareas, otro para las condiciones y así con los demás elementos que forman parte de una red \emph{YAWL}, el \textit{archivo.yawl} en el principio contiene información de los elementos y posteriormente la información gráfica de los mismos y las relaciones entre las tareas y/o condiciones.\\

\subsection{Parser de modelos YAWL}
Para la detección de un elemento en particular se utilizó código en primer lugar para obtener información del archivo construido por \textit{YAWL} y luego se procedió a filtrar los elementos que se deseaba obtener. Esto es debido a que no toda la información es necesaria como por ejemplo los iconos o imágenes que poseen algunos de estos modelos. A continuación se detallan fragmentos de código utilizado para la lectura de algunos de los elementos de estos modelos y la explicación correspondiente para la extracción de los datos de estos elementos.\\
Para la extracción de un elemento Task presente en el modelo, se crea una instancia de cada una de éstas almacenando información lógica como la relación que tendrá ésta con los demás elementos del modelo y la información gráfica que corresponde a las posiciones donde será bosquejada ésta misma, su etiqueta o nombre y las compuertas que pueda tener. A continuación un fragmento de código en el cual se podrá visualizar parte de esta información.

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=xml,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={template,id,text,name,split,numberBranch,join,flowsInto},
	tabsize=2, 
}
\begin{lstlisting}[caption=Elemento Task]
<task id="Calculate_Time_Out">
	<name>Calculate Time Out</name>
	<flowsInto>
		<nextElementRef id="unnamed_6" />
	</flowsInto>
	<flowsInto>
		<nextElementRef id="unnamed_4" />
	</flowsInto>
	<flowsInto>
		<nextElementRef id="unnamed_8" />
	</flowsInto>
	<join code="xor" />
	<split code="and" />
	...
</task>
\end{lstlisting}

\textbf{Obtencion de un elemento Task}\\
El método \textit{getElementsByTagName()} retorna una lista de elementos obtenidos del codigo XML. En el código siguiente se obtienen todos los elementos tasks del modelo y se obtiene solo el primero de ellos.

\begin{lstlisting}[caption=Atributo ID]

NodeList nodeTaskList = elem.getElementsByTagName("task");
Node taskNode = nodeTaskList.item(0);
Element taskNamed = (Element) taskNamedList.item(0);
NodeList nameTask = taskNamed.getChildNodes();
String name = ((Node)nameTask.item(0)).getNodeValue().toString();
newTask.setName(name);
\end{lstlisting}


\textbf{\\Atributo de un elemento del elemento Task}\\
El siguiente código detalla la captura de uno de los atributos del elemento Task. A modo de ejemplo se localiza en el archivo el atributo \textit{id}, el cual identifica al task del resto de de los elementos del modelo.

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={container,vertex,label,decorator,attributes},
	tabsize=2, 
}
\begin{lstlisting}[caption=Atributo ID]

NamedNodeMap taskElementList = taskElement.getAttributes();
Node aAttr = taskElementList.getNamedItem( "id" );
String idAux = aAttr.getNodeValue();
\end{lstlisting}

Lo mismo ocurre con el resto de los atributos como las coordenadas donde se dibujará el gráfico de este elemento, las entidades o elementos con las cuales tendrá asociación y la región de cancelación, se obtienen cada uno de ellos y se los almacena en la estructura Task correspondiente. Cuando una Task resulta ser compuesta, es decir, tiene asociado un submodelo, se la procesa de la siguiente manera. Cada subred posee un \textit{id} de la misma manera que las Task, entonces si una red tiene el mismo id que la Task, esta última resultara ser compuesta. Por lo tanto se genera una nueva instancia de la clase \textit{GUIDiagram} y se procesa los elementos de éste último de manera recursiva. Cada tarea puede tener su correspondiente compuerta \textit{split} o \textit{join}, éstas se analizan en un servicio distinto pero se lo asocia a la Task correspondiente.\\
Los elementos como las \textit{Conditions} los \textit{Inputs} y \textit{Outputs} se realiza con el mismo objetivo pero se captura distintos atributos, puesto que estos no poseen compuertas ni pueden generar submodelos como las Tasks.\\\newline

\textbf{Representación de coordenadas}
\\Para la obtención de las coordenadas, las cuales serán extraídas para realizar el ``dibujo'' de un determinado elemento, se procede de la siguiente manera. A modo de ejemplo será utilizado el ejemplo de la tarea que se trató anteriormente.


\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=xml,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={container,vertex,label,decorator,attributes},
	tabsize=2, 
}

\begin{lstlisting}[caption=Coordenadas del elemento Task]
<container id="Calculate_Time_Out">
	<vertex>
		<attributes>
			<bounds x="80,2" y="182,0" w="32,0" h="32,0" />
		</attributes>
	</vertex>
	<label>
		<attributes>
			<bounds x="55,0" y="213,0" w="96,0" h="38,0" />
		</attributes>
	</label>
	<decorator type="AND_split">
		<position>13</position>
		<attributes>
			<bounds x="111,2" y="182,0" w="11,0" h="32,0" />
			<size w="11" h="32" />
		</attributes>
	</decorator>
</container>
\end{lstlisting}


\begin{table}[htp]
        \centering
	\begin{tabular}{| l | c | p{7cm} |}
		\hline
		\multirow{10}{2cm}{\centering \textit{$<Task>$}} 	&   \textbf{Nombre}  & Multi-Choise\\
		\cline{2-3}
			& \multirow{6}{3cm}{\centering\textbf{Descripción}}	&	Representa la división de un flujo en dos o más flujos. Todos los flujos salientes se activan concurrentemente y en simultáneo. Cualquier cantidad de flujos salientes pueden ser activados, no es necesario que sea sólo uno, ni que sean todos ellos. También es llamado \textit{Conditional Routing}, \textit{selection}, \textit{OR-Split} o \textit{multiple choice}.\\
		\cline{2-3}
			&	\multirow{4}{3cm}{\centering\textbf{Ejemplo}}	&	Cuando una llamada de emergencia es atendida,
dependiendo de la naturaleza de la misma, se pueden iniciar las actividades de envío de la policía, del servicio médico y de los bomberos. Cualquier combinación de estas actividades puede ser disparada.\\
		\hline
	\end{tabular}
\end{table}

En el código superior se puede ver los distintos elementos que componen la realización del dibujo de un elemento Task. La información obtenida se asociara al elemento que se está analizando, entre ellos se puede mencionar:

\begin{itemize}
\item \textbf{Vertex:} Esta etiqueta contiene los datos representan la posición en el plano \textit{x} e \textit{y} indicando el punto superior izquierdo del elemento y el \textit{ancho} y el \textit{alto} del mismo. De esta manera se puede representar por ejemplo el Task calculando solo dos puntos, es decir las coordenadas \textit{(x,y)} y \textit{(x+ancho, y+alto)}. Esta información se almacena también en la instancia del objeto en cuestión.
\item\textbf{Label:} Aquí se puede obtener información para graficar, el nombre o texto que posee el elemento en el modelo. También se almacena en la estructura del elemento del modelo
\item\textbf{Decorator:} Esta etiqueta detalla el tipo y las coordenadas de la compuerta que posee el elemento del modelo. El tipo permite diferenciar entre los distintos tipos de compuertas. Los datos de esta etiqueta también se obtienen con el mismo procedimiento que se realiza con la etiqueta \textit{Vertex}.
\end{itemize}

Luego de que se haya analizado gran parte del código del modelo se procede a extraer información de \textit{flechas} o \textit{flows}. Éstas permiten que un elemento del modelo se relacione con otro incluso con las compuertas de cada una de las tareas, en caso de que éstas tengan. A continuación se detalla un fragmento para determinar la comunicación entre dos elementos.

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=xml,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={points,source,target,flow},
	tabsize=2, 
}
\begin{lstlisting}[caption=Coordenadas del elemento Flow]
<flow source="Modify_Pickup_Apm" target="unnamed_11">
    <attributes>...</attributes>
</flow>
\end{lstlisting}

Con mayor detalle se tiene que un \textit{flow} o \textit{flecha} tiene un elemento de origen y un elemento de destino ambos especificados por las etiquetas \textit{source} y \textit{target} respectivamente. Luego se tiene los puntos necesarios mediante los cuales será definida el \textit{flow}, en el ejemplo anterior cuenta con dos puntos pero en algunos casos puede presentar más haciendo que la misma no sea una recta lineal.\\

\newpage
\section{Representación del Modelo en FLWA}
Teniendo la información sobre la red y todos los elementos de la misma que se ha recolectado, se procede a representar dicha información de manera gráfica.\\ Para llevar a cabo esta tarea se creo una nueva clase \textit{GUIDiagram} que hereda atributos y métodos de la clase \textbf{Canvas}\footnote{Canvas: Clase del lenguaje de programación JAVA que permite el dibujo de formas geométricas o gráficos en dos dimensiones.}, la cual será la encargada de almacenar la información de los gráficos. Se re-definió en método \textit{paint(g)} este método es invocado constantemente luego de que una acción es realizada sobre la clase. De esta manera permite generar una secuencia de movimientos originando una animación.\\
Al igual como se lo realizó en el motor XML, con el objetivo de hacer comprensible el código, se creo métodos para el dibujado de las tareas, condiciones, flechas (relaciones entre elementos), compuertas, etc.\\

\subsection{Utilización de la clase Canvas}
Como se describió anteriormente para poder graficar cada uno de los elementos creados por \emph{YAWL}, fue necesario disponer de alguna librería que nos facilite este trabajo. La librería que se determino suficiente fue la de \textit{AWT} que pertenece a la API de JAVA. En particular se utilizó la clase \textit{Canvas}. Con el objetivo de poder definirse una interfaz propia y que responda a los eventos y comportamientos del usuario de una manera sencilla y personalizada se redefinió el método \textit{paint()} que posee la clase Canvas. Esta clase permite expresar cualquier figura geométrica en un plano y de esta manera se podrá representar todos los elementos recolectados en este plano. En definitiva este proceso de dibujado se realizará de manera similar a como se realiza esto en la herramienta \emph{YAWL}, es decir las tareas se representan como cuadrados, las condiciones se representan mediante círculos,etc.\\
A continuación se dará fragmentos de código de manera de facilitar la compresión del procedimiento utilizado para la representación de los elementos en \emph{FLWA}.\\\newline

\textbf{Representación de elementos Task\\}
Para dibujar un elemento Task dentro del Canvas se utilizó el siguiente método el cual permite dibujar un rectángulo si se le indica las coordenadas \textit{x},\textit{y} y el ancho y la altura del mismo.

\begin{shaded} 
\textit{drawRect(coordenada X, coordenada Y, ancho, altura)}
\end{shaded}

Para representar en el modelo o plano el nombre del Task se utilizó el siguiente método el cual requiere, el texto a mostrar y las coordenadas \textit{x} e \textit{y}.

\begin{shaded} 
\textit{drawString(texto, coordenada X, coordenada Y)}
\end{shaded}

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Representación de un Task]
gi.drawRect(task.getX(), task.getY(), task.getWidth(), task.getHeight());
if(task.isComposite())
	gi.drawRect(task.getX()+5, task.getY()+5,task.getWidth()-10, task.getHeight()-10);
if(task.getName() != null){
	gi.drawString(task.getName(), task.getLabX(),task.getLabY());
}
\end{lstlisting}

Como se puede notar en el fragmento de código anterior, este proceso se realiza por cada tarea presente en el modelo. Se realiza el rectángulo que va a representar el elemento Task, y posteriormente se analiza si éste es un Task del tipo compuesto, entonces se realiza un rectángulo mas pequeño que lo diferencia de los que no lo son. Finalmente si este elemento posee un texto a mostrar se lo grafica con el método antes detallado.\\\newline

\textbf{Representación de elementos Condition\\}
Para representar los elementos Conditions en el modelo se utilizó el siguiente método el cual requiere, al igual que lo requerido para dibujar un Task, las coordenadas \textit{x} e \textit{y} y el ancho y alto; solo que en esta ocasión se dibujará un circulo en lugar del rectángulo.

\begin{shaded} 
\textit{drawOval(coordenada X, coordenada Y, ancho, altura)}
\end{shaded}

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Representación de un Condition]
gi.drawOval(cond.getX(), cond.getY(), cond.getWidth(), cond.getHeight());
gi.setColor(Color.BLACK);
if(cond.getName() != null)
	gi.drawString(cond.getName(), cond.getLabX(),cond.getLabY());
\end{lstlisting}

Como se ve el el código anterior se realizar el circulo que representa el Condition con el método mencionado, luego se dibuja el texto que lo representa como se realizo con los Task. Este procedimiento realizado para representar los elementos Conditions también se realiza para los \textit{Input Conditions} y los \textit{Output Condition} los cuales carecen de texto para mostrar y poseen un circulo coloreado. Para lograr éste último se debe utilizar un método diferente pero que requiere los mismos parámetros que en el caso de un Condition.

\begin{shaded} 
\textit{fillOval(coordenada X, coordenada Y, ancho, altura)}
\end{shaded}

\textbf{Representación de Flechas o Flows\\}
Como se comentó en la captura de estos elementos, sólo es necesario para la representación de éstas últimas al menos dos posiciones en el plano, estos dos puntos representarán el origen y el destino de la flecha. Como vimos anteriormente cada flecha recolectada tiene la información de cuáles deben ser los elementos (origen y destino). Ahora bien, estos elementos pueden ser tanto Task como Condition y en caso de Task pueden tener compuertas o no. Se deberá analizar si tiene compuerta para que sea ésta la referencia a la cual la flecha pueda apuntar, es decir si la tarea origen contiene una compuerta \textit{split} será la referencia del origen de la flecha o si la tarea destino posee una compuerta \textit{join} será la referencia del destino de la flecha. Como consecuencia a esto se debe configurar los puntos de origen y de destino antes de dibujar la flecha.
Para la realización del dibujo de una flecha, teniendo los dos puntos necesarios, se utilizó el siguiente método que requiere las coordenadas del punto de origen y las coordenadas del punto destino.

\begin{shaded} 
\textit{drawLine(origen X, origen Y, destino X, destino Y)}
\end{shaded}

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Representación de un FLow]
Point pointS = currentFlow.getCoordenates().get(p);
Point pointT = currentFlow.getCoordenates().get(p+1);
gi.setColor(Color.BLACK);
gi.drawLine(pointS.x,pointS.y,pointT.x,pointT.y);
\end{lstlisting}

Durante el proceso de representación de los \textit{flows} se va obteniendo cada par de puntos y se los dibuja en medida que se obtiene. Existen casos en los que se puede tener cantidad impar de estos puntos por lo cual se deberá tratar de la siguiente manera; el primer punto con el segundo y luego el segundo nuevamente con el tercero, en el escenario de flecha con tres puntos. En conclusión si se tiene diferentes cantidades de puntos estos serán representados mediante una flecha formado por una linea(para el caso de un sólo par puntos) o por mas de una linea (para el caso de mas de dos puntos).\\\newline
La punta de la flecha o \textit{arrowhead} se realiza mediante un calculo geométrico, ya que varía su inclinación según la posición del elemento destino. Es decir, si una flecha apunta a un elemento en sentido \textit{norte-sur} y este elemento cambia de posición de manera que el sentido de la flecha cambie ahora a por \textit{sur-norte}, la posición de la punta de la flecha cambia también. El siguiente fragmento de código muestra como se consiguió esto, parte del fragmento fue extraído de \cite{arrowhead} y fue modificado según lo necesario.


\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Representación del Arrowhead]
Polygon tmpPoly=new Polygon();
double aDir=Math.atan2(startX-endX,startY-endY);
int i1=12+(int)(arrowHeadSize*2);
int i2=6+(int)arrowHeadSize;
tmpPoly.addPoint(endX,endY);
tmpPoly.addPoint(endX+xSin(i1,aDir+0.5),endY+yCor(i1,aDir+0.5));
tmpPoly.addPoint(endX+xSin(i2,aDir),endY+yCor(i2,aDir));
tmpPoly.addPoint(endX+xSin(i1,aDir-0.5),endY+yCor(i1,aDir-0.5));
gi.fillPolygon(tmpPoly);
\end{lstlisting}

Este código hace uso de \textit{Polígonos} otra forma de poder dibujar que ofrece la clase Canvas. Básicamente lo que se consigue es obtener el ángulo representado por la tangente de los puntos origen y destino de la flecha mediante el método \textit{Math\.atam2(...)}. Posteriormente al polígono se le agregan puntos correspondientes al ángulo de la flecha de manera que formen la punta de la misma de manera correcta.\\\newline

\textbf{Representación de Compuertas\\}
Este último elemento como se dijo en capítulos anteriores puede variar según el modelo, pero solo existen algunos tipos de compuertas que son las que se detallaron en el capítulo 2. \emph{YAWL} a estas compuestas las gráfica mediante el uso de una librería como Canvas y cálculos de puntos para graficar las mismas. Es por esto que se decidió utilizar la misma idea y graficar las compuertas haciendo uso de los servicios que nos ofrece esta clase. Para lograr esto, en particular se podría utilizar el método \textit{drawPolygon()} pero debido a su facilidad de uso y la experiencia con el mismo se decidió hacer uso del método presentado anteriormente el cual permite dibujar lineas \textit{drawLine()}.
Con este procedimiento se podrá representar cada una de las compuertas, es decir tanto las que estén configuradas como \textit{join} o las que estén como \textit{split}. El tipo de compuerta puede variar en \textit{AND},\textit{OR} o \textit{XOR}. Existen casos en que estas compuertas están a los lados izquierdo y derecho de cada elemento Task, pero también puede haber casos en que esto varía. Es decir, que puede un tarea tener una compuerta el en lado superior de la misma y otra en el lado izquierdo o también en el lado derecho y así con cada combinación. Esto hace mas complicado la representación de las compuertas ya que antes de realizar el modelo se debe analizar los casos.

\subsection{Tecnica ``Double Buffer'' y \textit{Anti-Aliasing}}
Por cada cambio producido se redibuja completamente todo el modelo, es decir, si se desea cambiar tan solo una tarea de posición se va repintar todo el modelo. Esto se podría optimizarse redefiniendo el método \textit{paint} de manera que se pueda detectar que elementos fueron los alterados y repintar solo estos, debido a que no es objetivo de este proyecto no aplicaran estas modificaciones en la implementacion del mismo. Por otra parte el redibujar todo nuevamente genera un efecto de destello el cual resulta desagradable para el usuario.\\
 Para evitar que cada cambio producido refresque el dibujo haciendo inapropiado para el uso, se uso la técnica de \textit{Doble Buffer} la cual consiste en realizar una acción sobre el dibujo principal, se crea una segunda imagen y los cambios se verán reflejados en ésta última y una vez completado el dibujo nuevo se utiliza ésta última como imagen principal. Esto produce una apreciación al estilo de una animación de los elementos del modelo de manera agradable sin que la pantalla realice destellos.\\\newline
Por último, para ayudar a la estética de los elementos representados en la herramienta, se procedió a utilizar un servicio que brinda la clase \textit{Graphics2D} el cual permite generar unas estructuras más definidas y con menos ```poligonos''. Este filtro se aplica a cada uno de los elementos que sea representados luego de la llamada del mismo.

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={Graphics2D,KEY_ANTIALIASING},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Coordenadas de un evento]
Key antialiasing = RenderingHints.KEY_ANTIALIASING;
Key valueAntialias = RenderingHints.VALUE_ANTIALIAS_ON;
Graphics2D g2d = (Graphics2D)gi;
g2d.setRenderingHint(antialiasing,valueAntialias);
\end{lstlisting}

Esta técnica consiste en habilitar el \textit{anti-aliasing} el cual mejora el detalle de los elementos eliminando poligonos restantes, sin embargo requiere un uso mayor del procesador puesto que es costoso en recursos computacionales. De todas maneras es un proceso simple para gráficos en dos dimensiones y elementos geométricos sencillos. 

\section{Representación de Fluentes}
\subsection{Introducción}
En esta sección detallamos la implementación de la funcionalidad de \emph{FLWA} que permite la definición de fluentes, su creación y definición. Como lo mencionamos en 4.2.2, estos fluentes permiten describir estados abstractos del modelos que pueden ser utilizados en la definición de propiedades a analizar. Se presentará la tecnología utilizada para su implementación, como así también, fragmentos de código para ejemplificar y ayudar al lector a comprender lo realizado. Por otro lado, también se presentará la representación de los fluentes en forma gráfica mediante arboles y las definiciones gráficas de los mismos sobre el modelo.

\subsection{Definición de fluentes}
Como se comentó a lo largo de los capítulos de este trabajo, la herramienta desarrollada permite la definición de fluentes. Esta idea que se detalló en el capítulo 4, consiste en poder expresar y configurar un fluente de forma gráfica. Como parte a esta solución se propuso que el usuario permita la definición de los mismo y además pueda ver el contenido que posee, es decir, que se permita visualizar los elementos (eventos del modelo) que conforman la definición del fluente.\\ En un principio se pensó que lo mejor podría ser una tabla pero esta resultaría confusa al momento de representar los elementos de un fluente si estos alcanzan un número elevado. Por este motivo se decidió implementar una estructura jerárquica donde se pueda ver el fluente definido y presentarlos de manera gráfica en forma de árbol. Esta estructura de árbol se puede realizar a través del lenguaje JAVA mediante la clase JTree, esta clase permite definir nodos y a estos poder definirles sub-nodos y hojas.\\\newline

Tomando esta idea y teniendo en cuenta la definición de un fluente, se decidió definir la siguiente estructura, la cual se muestra a modo de ejemplo en la Figura 5.3.

\begin{shaded}
$$fluent A = \langle\{ Task1.start,Task4.end\}, \{Task2.end,Task3.start,Task6.end\}\rangle$$
\end{shaded}

El siguiente diagrama expresa a modo de ``árbol'' el \textit{fluente A}.

\begin{figure}[htp] \centering{
\includegraphics[scale=0.50]{graphs/fluent.pdf}}
\caption{Diseño de la representación de Fluentes}
\end{figure}

Como se ve en la figura se utilizará un esquema de exploración por nodos, el cual estará formado por.
\begin{itemize}
\item\textbf{Nodo Raíz:} Este nodo representa el fluente que se ha definido, éstos contendrán la información oculta o visible según se prefiera. También brinda la posibilidad de cambiar de nombre manteniendo la regla de que ningún fluente puede tener un nombre que empiece con números o caracteres especiales.
\item\textbf{Nodo On:} Este nodo es el encargado de contener todos los eventos del modelo que hacen que el fluente se encienda o hace que el  ``prendido''. No posee la misma característica que el nodo raíz
\item\textbf{Nodo Off:} Este nodo es muy similar al nodo On solo que éste tiene la información de eventos que hacen que el fluente se ``apague''.
\item\textbf{Hoja Event:} En el gráfico se representa como nodo pero no puede contener elementos dentro. A este nivel sólo se tiene los eventos elegidos que configuran el fluente.
\end{itemize}

\subsection{Eventos utilizados para fluentes}
Como se pudo detallar en el capítulo anterior, junto a la función de definición de propiedades que será analizado en la sección siguiente, se puede definir los fluentes y configurarlos mediante el uso de diferentes eventos que ofrece la capa de aplicaciones de JAVA. Estos eventos permiten capturar ciertas acciones del usuario y realizar una tarea o ciertas acciones con el resto de los componentes de la herramienta.
En lo que respecta a la definición de fluentes y su correspondiente configuración, se de los siguientes eventos proporcionados por el lenguaje. Algunos de estos eventos han sido redefinidos con el objetivo de controlar mejor las acciones que desencadene el mismo.\\\newline

\textbf{MouseMotionListener:} Ésta es una interfaz la cual permite definir los diferentes momentos que se puede obtener de la acción de mover el \textit{Ratón}. Esto quiere decir que es posible registrar o desencadenar una acción, para el caso de los fluentes este tipo de evento nos da la facilidad de registrar un \textit{Drag-and-Drop} es decir un movimiento que se da cuando se quiere ``arrastrar'' un fluente y utilizarlo en la definición de propiedades.\\\newline

\textbf{MouseLister:} Esta interfaz, a diferencia de la anterior, no registra los eventos que surgen por un desplazamiento del \textit{Ratón}, sino por el contrario registra aquellos que suceden cuando se realiza un \textit{click}, cuando se los suelta o cuando se mantiene presionado el botón del \textit{Ratón}.
Este tipo de evento fue el utilizado también para realizar los movimientos de los diferentes elementos del modelo, por ejemplo, para cambiar la posición de los mismo y también utilizado para lograr la representación de las regiones de cancelación.\\\newline

Utilizando estos eventos mediante las coordenadas \textit{x} e \textit{y} de donde fue presionado el boton del Raton, se puede calcular la misma.
\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Coordenadas de un evento]
if((e.getX() > cTask.getX()) && (e.getX() < (cTask.getX() + cTask.getWidth()/2)) 
&& (e.getY() > cTask.getY()) && (e.getY() < (cTask.getY()+ cTask.getHeight()))){
	Object[] taskOn = {cTask,true,this.getId()};
}
\end{lstlisting}

Una vez realizada la acción del raton y si ésta coincide con las coordenadas de regiones para el registro de los eventos de alguna de las Task del modelo, se procede a la captura del mismo y se genera una estructura que determina a que tarea o Task hace referencia, un valor para determinar si es de encendido o apagado (del fluente) y por último un indicador a que modelo se le aplico esta acción, puesto que puede haber mas de un modelo. La estructura generada es almacenada por el fluente que se está definiendo y posteriormente se realiza el gráfico del mismo.

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Representación de un evento]
Object[] taskOn = currentFluent.getListOn().get(i);
if(((String)taskOn[2]).compareTo(this.getId())==0){
 if((Boolean)taskOn[1]){
  Task task = (Task) taskOn[0];
  gi.setColor(new Color(0, 250, 0));
  gi.fillRect(task.getX(), task.getY(), task.getW()/2, task.getH());
  gi.setColor(new Color(0, 150, 0));
  gi.drawRect(task.getX(), task.getY(), task.getW()/2, task.getH());
 }else{
  Task task = (Task) taskOn[0];
  gi.setColor(new Color(0, 250, 0));
  gi.fillRect(task.getX()+task.getW()/2, task.getY(), task.getW()/2, task.getH());
  gi.setColor(new Color(0, 150, 0));
  gi.drawRect(task.getX()+task.getW()/2, task.getY(), task.getW()/2, task.getH());
 }
}
\end{lstlisting}

Este fragmento de código detalla la representación de un evento que ``prende'' (torna verdadero) el fluente, denotado gráficamente con el color verde. Para caso de eventos que desactivan fluentes, la notación gráfica es con color rojo.
Para los casos en los cuales un fluente es activado o desactivado por eventos que pertenecen a una tarea compuesta, es decir, están gráficamente representados en un \emph{tab} que contiene el workflow que la define, se muestra al lado del nombre de dicha pestaña un ícono indicando que el fluente tiene eventos que lo definen en el workflow contenido en ella.

\subsection{Cursores de definición de eventos}
Para la configuración de los fluentes como se comentó en el capítulo 4, se realiza mediante la selección de diferentes cursores los cuales determinaran el tipo de acción que se quiere realizar.
La aplicación actualmente posee cuatro tipo de cursores los cuales serán descriptos a continuación.\\\newline

\textbf{Cursos de Selección:} Este cursor se describe como un cursor normal, con la propiedad de poder seleccionar y editar la visualización del modelo. Además se podrá visualizar las compuertas de la tarea selecciona y las regiones de cancelación; para éstas últimas mediante un ``double-click''.\\\newline
\textbf{Cursor On:} Este tipo de cursor se representa como el anterior pero además presente un punto de color verde. Éste se utiliza para definir los eventos cuya ocurrencia activará el fluente seleccionado.\\\newline
\textbf{Cursor Off:} El cursor Off es similar al anterior pero en lugar de tener un punto de color verde es rojo, y se utiliza con el mismo propósito pero para seleccionar en que eventos se va desactivar el fluente seleccionado.\\\newline
\textbf{Cursor Borrador:} Este último cursor se puedo ver una flecha de punta mas pequeña y con una imagen de goma de borrar. Tiene la funcionalidad de borrar cualquier evento seleccionado, es decir, borrar de la definición del fluente seleccionado aquellos eventos que seleccionan (en caso de estar presente en dicha definición).\\\newline

Para la definición de estos cursores fue necesario usar diferentes servicios que ofrece el lenguaje, el siguiente fragmento de código representa la definición de uno de los cursores.
\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Definición de un cursor]
public void setOnMouse() {
	try {
		Toolkit tool = Toolkit.getDefaultToolkit();
		Image image = tool.createImage(getClass().getResource("/icon/pointerOn.png"));
		Cursor cursor = t.createCustomCursor(image, new Point(0, 0), "selectionOn");
		this.setCursor(cursor);
		cursor = this.getCursor();
	} catch (IndexOutOfBoundsException e) {
		e.printStackTrace();
	} catch (HeadlessException e) {
		e.printStackTrace();
	}
}
\end{lstlisting}

Este código representa la definición de lo que representa el cursor de selección de eventos \textit{on} o dicho de otra manera los eventos que hacen que el fluente se active. Por un lado se obtiene la imagen que va representar el cursor y por el otro se crea el mismo con las características como el identificador, que en este caso es \textit{selectionOn} y el punto de acción. Por último, una vez creado el cursor se lo asigna a la pantalla, como uno de los posibles cursores.
De esta manera, se crean los diferentes cursores y se los asigna según la elección del usuario a la pantalla principal de \emph{FLWA}. Cuando esto ocurre, si se realiza un evento con el cursor elegido, se analiza primero que tipo de cursor es mediante el identificador y luego se determina las coordenadas del mismo como se detalló en la sección anterior.

\section{Representación de propiedades}
\subsection{Introducción}
Como objetivo fundamental de \emph{FLWA}, es la definición de propiedades que luego serán verificadas posteriormente por \emph{LTSA}. La definición de las mismas es un proceso un tanto simple pero resulta complejo cuando se designan diferentes alternativas para conseguir un mismo resultado. Es por esto que en esta sección se analizara las diferentes alternativas para la construcción de las diferentes fórmulas. También se presentara una utilización de los fluentes definidos ya que éstos toman importancia cuando son parte de la misma fórmula a definir y luego verificar. Por último se detallará el uso de la definición de las plantillas definidas y cómo se las procesa.

\subsection{Definición de propiedades}
Como se comentó a lo largo del trabajo, el desarrollo está centrado a la definición de las propiedades. Éstas son creadas por el usuario y dependen directamente del modelo del cual se está trabajando. Para la definición de las mismas, se tomo la idea de que cada propiedad creada puede ser visualizada en la pantalla principal y que éstas tengan la posibilidad de ser tildadas o no para su verificación, según se prefiera.  Otra funcionalidad ofrecida por \emph{FLWA} es brindar como alternativa a la escritura por parte del usuario de los operadores lógicos, es una barra de herramientas que permite incorporarlos, mediajte \emph{drag and drop}, a la fórmula.\\\newline

Para de la creación de las propiedades se utiliza una estructura \textit{PanelArea} que contiene los elementos que formarán un espacio de texto y otros elementos mas para le creación de la misma. Entre los más significativos se puede mencionar al cuadro de texto, creado mediante \textit{JTextArea} el cual permitirá escribir la fórmula, un \textit{JLabel} para indicar el número de fórmula, el campo para indicar si está habilitada o no \textit{JCheckBox} y por último un \textit{JPopupMenu} para ofrecer al usuario los elementos que podría utilizar para crear la fórmula. La creación de esta estructura es variable, ya que el usuario define la cantidad de propiedades que desea.
La creación de cada fórmula se inició cuando el usuario acciona el botón \textit{Add Property}, entonces se utiliza el siguiente código para crearla.

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Definición de un cursor]
public PanelArea addNewAreaPanel(){
	numberProperty++;
	PanelArea newAreaPanel = new PanelArea(numberProperty,vectorTask);
	newAreaPanel.setActionListener(new AddPropertyMediator());
	listPanelAreas.addLast(newAreaPanel);
	getAreasPanel().add(newAreaPanel);
	
	return newAreaPanel;
}
\end{lstlisting}

Este código crea la estructura que se describió anteriormente y con su correspondiente número de identificación, luego se carga el elemento que lo va a controlar y por último se agrega al final del resto del conjunto de propiedades definidas. Por último se actualiza la pantalla principal. \\
Se puede notar que al momento se crear la estructura \textit{PanelArea} se se invoca el constructor con un elemento llamado \textit{vectorTask}, este parámetro contiene todos los elementos Task del modelo. Esto se realiza con el objetivo de ofrecer al usuario estos elementos para que los pueda elegir siendo ésta otras de las alternativas al momento de crear las propiedades. Para lograrlo, los elementos Task que contiene el vector son transferidos al atributo del tipo \textit{JPopupMenu} para crear un menú emergente y ofrecer los elementos con sus diferentes eventos.
Los acciones que se produzcan sobre el menú fueron administrados por los siguientes eventos:

\begin{itemize}
\item\textbf{MouseListener} Para este tipo de interfaz se definió una instancia de ella que va determinar las acciones que el usuario desea utilizar, en este caso se tomaran los eventos como \textit{MouseEvent} producidos por el ratón y se los gestionará a través de \textit{MouseAdapter} el cual permitirá administrar los eventos cuando se presiona el botón del ratón, cuando se lo suelta, cuando se lo mantiene, etc.
\item\textbf{KeyListener} Sucede de manera similar al uso del ratón, solo que éste determina las acciones que provienen del teclado, estos eventos son del tipo \textit{KeyEvent}. Con el mismo procedimiento se registran los diferentes estados de una tecla del teclado mediante la interfaz \textit{KeyAdapter}.
\end{itemize} 

Además de la propiedad que posee la estructura \textit{PanelArea}, también se le brinda la posibilidad de poder disponer de los fluentes que se han definido. Esto es posible mediante el uso de elementos ofrecidos por el lenguaje como los elementos de la familia \textit{JComponent}. Estos elementos tienen la posibilidad de transferir cierta información de un elemento de esta familia a otro totalmente diferente pero también proveniente de la misma familia. Mediante esta funcionalidad se puede transferir por ejemplo el texto de un elemento \textit{JLabel} a otro \textit{JList}.
El siguiente fragmento de código refleja el uso de esta característica.



\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Manejador de elementos JComponent]
targetArea = (JTextArea) c;
if (t.isDataFlavorSupported(DataFlavor.stringFlavor)) {
	str = ((String) t.getTransferData(DataFlavor.stringFlavor)).toLowerCase();
	if(str.equals("\\/") || str.equals("/\\") || str.equals("->") || 
	str.equals("W") || str.equals("X")){
		targetArea.insert("(  "+str+"  )", targetArea.getCaret().getDot());
	}else if(str.equals("[]") || str.equals("<>") || str.equals("!")){
		targetArea.insert(str+"(  "+"  )", targetArea.getCaret().getDot());					
	}else{
		if(str.contains(":")){
			str = str.substring(str.indexOf(":")+1, str.length());
		}
		targetArea.insert(" "+str.toUpperCase()+" ", str.getCaret().getDot());
	}
} else {
	System.out.println("the import fail");
	return false;
}
\end{lstlisting}

Cuando se desea manejar la información que se va a transferir de uno de estos elementos a otro es necesario crear una clase del tipo \textit{TransferHandler} en la que se va a indicar como se desea transferir esta información. Esto permite evitar la existencia de alguna ambigüedad ya que por ejemplo se podría tener un elemento \textit{JTable} con varias filas de diferente tipo de información y se desea transferir cierto tipo de información a otro elemento del tipo \textit{JTextField}, se debe ser explícito qué información de la tabla va ser transferida al cuadro de texto. Por otro lado es importante mencionar que se puede especificar las condiciones en que se va transferir esta información, es decir, se podría decidir qué información transferir en ciertos casos y cuándo no transferirla. Como condición para que ambos componentes de la familia \textit{JComponent} se comporten de la manera deseada es necesario configurarlos de la siguiente manera. Por un lado, con una instancia de la clase \textit{TransferHandler} el elemento que va recibir la información administrada proveniente de otro elemento.

\begin{shaded}
jTextArea.setTransferHandler(new TreeHandler());
\end{shaded}

Por el otro lado se debe indicar al elemento que va poder enviar información al elemento anterior. Esto se consigue mediante el siguiente método.

\begin{shaded}
jTree.setDragEnabled(true);
\end{shaded}

De esta manera se consigue transferir información de un elemento \textit{JTree} a otro del tipo \textit{JTextArea} mediante una acción de \textit{Drag-and-Drop}. En \emph{FLWA} se utilizó solo dos de este tipo de transferencia de información, uno de ellos sucede cuando se quiere usar los operadores que se ofrecen en la pantalla principal y el segundo de ellos ocurre cuando se desea utilizar alguno de los fluentes de los que se han definido en alguna de las propiedades. Esto permite encapsula información en los fluentes y usarlos en una de las propiedades sencillamente ``arrastrandolos'' hacia la posición conveniente. La transferencia de los operadores fue reemplazada por una representación de ellos utilizando los caracteres \textit{unicode}\footnote{Unicode es un estándar de codificación de caracteres diseñado para facilitar el tratamiento informático, transmisión y visualización de textos de múltiples lenguajes} los cuales serán traducidos a su representación original cuando la propiedad que los contenga sea verificada.


\section{Plantillas de Propiedades}
En esta sección se presentará otra alternativa al momento de crear propiedades. Esta alternativa, como se comentó en el capítulo anterior, se da en forma de plantillas que el usuario podrá utilizar o incluso crear nuevas plantillas, modificarlas o tal vez eliminarlas o reemplazarlas. 
Para el uso de estas plantillas es necesario disponer del archivo \textit{templates.xml} ya que la ausencia de éste inhabilitaría la posibilidad de contar con las mismas.
Con el objetivo de hacer entendible el uso de éstas, se tomó como guía a \textit{Declare} que realiza esto de una manera muy sencilla y eficiente.\\
El módulo encargado de utilizar las plantillas cuenta con dos partes fundamentales, una de ellas es la interpretación y almacenamiento temporal de las plantillas definidas en el archivo mencionado, y el otro es la encargada de mostrar éstas en una pantalla adicional y realizar el proceso de traducción que detallaremos en 5.9.1.

\subsection{Interpretación de Templates}
Este proceso requiere de tomar las plantillas o \textit{Templates} definidas en un archivo con formato XML y poder almacenarlas en una estructura y luego visualizarlas en pantalla. Como las plantillas están almacenas desde un principio en el archivo usando el lenguaje \textit{xml} se puede utilizar el mismo mecanismo ya utilizado para la interpretación de los modelos \emph{YAWL}.
Por tal motivo se utilizó, nuevamente la librería DOM que ofrece la capa de servicios de JAVA.\\ La estructura de las plantillas es la que detalló en el capítulo 4, esta estructura posee atributos obligatorios que serán requeridos por \emph{FLWA} y opcionales que brindan información adicional que puede ser útil al momento de utilizar cierto Template. La siguiente tabla detalla los campos y qué restricción existe sobre ellos.\\\newline

\textbf{Obligatorios:}
\begin{itemize}
\item\textbf{Id:} Este atributo representa el identificador de la plantilla que las diferencia del resto.
\item\textbf{Text:} Éste es el campo con mayor relevancia, ya que contiene la fórmula que será procesada por un mecanismo de traducción usando los elementos del modelo y los fluentes definidos. Cabe destacar que la codificación con la cual se escribe la misma, es decir que los caracteres especiales deben ser expresados como ``tags'' del lenguaje \textit{HTML/XML}.
\item\textbf{Number of Branch:} Este atributo representa los parámetro requeridos para utilizar la plantilla elegida. Cada parámetro determina un elemento del modelo por el cual es instaciado al momento de la definición de la fórmula.
\end{itemize}

\textbf{Opcionales:}
\begin{itemize}
\item\textbf{Description:} Si bien no es obligatorio, este campo es de suma importancia ya que describe en lenguaje natural lo que expresa la fórmula. En caso de fórmulas complejas puede detallar la forma de instanciar sus parámetros para que su aplicación sea correcta.
\item\textbf{Display:} Este campo no es mas que decorativo, no tiene usos importantes sino el de representar en pocos caracteres un símbolo del template definido.
\item\textbf{Name:} Es el nombre para denotar la plantilla.
\item\textbf{Image:} Almacena la dirección (path) donde se encuentra la imagen que describe gráficamente la plantilla.
\end{itemize}

Estas plantillas serán cargadas sólo si el usuario desea utilizar el módulo de elección de platillas.\\

\subsection{Representación de Plantillas de Propiedades}
Una vez procesado el archivo de plantillas se procesan las estructuras que almacenan la información recolectada y se los visualiza en una nueva ventana gráfica. En ella se visualizará la lista en forma de exploración de árbol, similar a la utilizada para la definición de fluentes. Cuando el usuario selecciona alguna de las plantillas, se visualiza la información de la misma y se genera tantos campos como cantidad de parámetros tenga la plantilla.


\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Representación de Plantillas de Propiedades]
public void loadTemplateInPanel(Template template){
	this.parametersPanel.setVisible(false);
	this.descriptionLabel.setText(template.getDescription());
	this.previewLabel.setIcon(template.getImage());
	for(int i=0;i<template.getNumberBranch();i++){
		ParameterPanel parameter = new ParameterPanel(i);
		listPanelTask.add(parameter);
	}
	this.parametersPanel.setVisible(true);
}
\end{lstlisting}

El código anterior detalla cómo se carga una plantilla seleccionada en la ventana principal.

\subsection{Traducción de Plantillas de Propiedades}
Este proceso se realiza, en base a las fórmulas que han sido recolectadas del archivo \textit{templates.properties}. Éstas contiene como representación de cada parámetro una letra del abecedario, esto significa que para que el proceso de traducción sea exitoso, la fórmula cargada en el archivo debe ser correcta. Cuando el usuario decide colocar en cada uno de los parámetros un fluente o un evento del modelo utilizado, lo que realmente está diciendo es; que el primer parámetro lo reemplace por lo que se haya elegido, el segundo sea reemplazado por lo elegido y así sucesivamente. De esta manera si el usuario completa todos los parámetros y decide confirmar el uso de la plantilla elegida, recién en ese momento se traduce la fórmula.


\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={drawRect,drawString},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Traducción de Plantillas de Propiedades]
if(!isFluent(this.listTaskPanel.get(i).getTaskField().getText())){
	property = property.replaceAll(String.valueOf(((char)(i+65))),
	this.listTaskPanel.get(i).getTaskField().getText().toLowerCase());
}else{
	property = property.replaceAll(String.valueOf(((char)(i+65))),
	this.listTaskPanel.get(i).getTaskField().getText());
}
\end{lstlisting}

El código anterior muestra el tratamiento especial si el parámetro va ser reemplazado por un fluente o por un evento del modelo. Esto se debe a que el nombre de los fluentes puede variar según sea modificado por el usuario. Luego del tratamiento, se procede a reemplazar las letras de la fórmula de la propiedad por los parámetros elegidos mediante el uso de un servicio llamado \textit{replaceAll} perteneciente a la clase String\footnote{Clase del lenguaje JAVA que ofrece una lista de servicios para el uso y tratamiento de textos o cadenas de texto} el cual permite el reemplazo de todas las ocurrencias de un texto por otro sobro la cadena principal. Luego del proceso de traducción se agrega la nueva fórmula al resto de las fórmulas definidas en la página principal.

\section{Verificación de propiedades}
Aquí se presenta una de las tareas más relevantes, como objetivo del trabajo, que es el proceso de verificación. Éste proceso realiza la comunicación con \textit{yawl2fsp} y \textit{LTSA} en dos etapas que se detallarán a continuación. En primer lugar el uso de \textit{yawl2fsp} para la traducción del modelo y el tratamiento de esta traducción para la inclusión de las propiedades y en segundo lugar, se dará una descripción de los procesos para el tratamiento y verificación de las propiedades mediante la herramienta \emph{LTSA}.

\subsection{Traducción de propiedades a FSP}
Cuando se tienen las propiedades definidas y se desea verificar las mismas, se realiza un tratamiento a estas propiedades y a los fluentes que forman parte de las mismas. Para ello en necesario disponer de la traducción completa del modelo en cuestión, es por esto que se hace uso de la herramienta \textit{yawl2fsp}, la cual nos genera dicha traducción como un proceso \emph{FSP}, como fue detallado en 2.5.\\
Esta traducción que realiza \textit{yawl2fsp} involucra sólo la información de las tares, las condiciones o todo lo relacionado con los elementos del modelo pero no las propiedades y fluentes definido en \textit{FLWA}. Esto se debe a que son dos herramientas diferentes y la comunicación está dada por el input que se le brinda a \textit{yawl2fsp} y el output que se obtiene de la misma, siendo \textit{yawl2fsp} una herramienta que se ejecuta por linea de comando (no posee interfaz gráfica). Se invoca a \textit{yawl2fps} con el modelo como imput y el resultado es la especificación del mismo mas un servicio de \textit{mapping}, que será detallado en secciones posteriores.

\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={Process,String\[\]},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Invocación de \textit{yawl2fsp}]
String[] cmd = {"java","-jar","yawl2fsp.jar","--info="+mapper,yawlFile,lts};
Process p = Runtime.getRuntime().exec(cmd);
\end{lstlisting}

Como lo muestra el código anterior, la invocación a \textit{yawl2fsp} se lleva a cabo mediante el uso de la clase \textit{Runtime} la cual permite arrojar otro hilo de ejecución, la ejecución un comando. Este comando requiere de parámetros y para el caso presentado a continuación se detalla cada uno de los parámetros utilizados.
Como cualquier ejecución de un paquete en el lenguaje JAVA se debe hacerlo mediante el uso de \textit{java -jar}, luego el tercer parámetro representa la librería a utilizar

\begin{center}
	\begin{tabular}{| c | p{8cm} |}
		\hline
		\textbf{Parámetro} 	&   \textbf{Descripción}  	\\
		\cline{1-2}
		\textbf{java} 	&   Representa en lenguaje utilizado. Es obligatorio.\\		
		\cline{1-2}
		\textbf{-jar} 	&   También es obligatorio y representa el tipo de paquete que se ejecutará.\\		
		\cline{1-2}
		\textbf{yawl2fsp.jar} 	&   Este campo es el propio paquete que se va a ejecutar, en el se contiene a la herramienta en el lenguaje \textit{bytecode} que será interpretado por la maquina virtual de JAVA.\\		
		\cline{1-2}
		\textbf{--info=mapping} 	&   Es opcional y representa la ubicación absoluta y nombre del \textit{mapping} que generará la herramienta la cual va ser de gran utilidad para la traducción de los elementos del modelo.\\		
		\cline{1-2}
		\textbf{yawlModel} 	&   Este campo es requerido puesto que es el modelo del cual se pretende tener la traducción, es la ubicación absoluta del modelo creado por \textit{YAWL}.\\		
		\cline{1-2}
		\textbf{output} 	&   Por último este parámetro es el resultado de la traducción del modelo que le señalamos anteriormente.\\
		\cline{1-2}
		\hline
	\end{tabular}
\end{center}
	
El resultado de ejecutar la herramienta \textit{yael2fsp} con estos parámetros es: por un lado la especificación del modelo, y por el otro, un archivo serializado que contendrá un \textit{mapping} entre los nombre del modelo y los nombres utilizados en la especificación. \\
El paso siguiente, es la incorporación de las propiedades y fluentes definidos dentro de la especificación conseguida. Para lograr esto es necesario el uso del mapping generado debido a que \textit{yawl2fsp} realiza la especificación pero ésta no conserva los nombres del modelo. De esta manera se debe traducir los elementos que forman las propiedades a los correspondientes nombres utilizados en la especificación.
La herramienta \textit{yawl2fsp} sirve además como librería de los servicios que serán de gran utilidad para la traducción
de los nombre utilizados. En primer lugar el método

\begin{shaded}
FLWAtoFSP.load("flwa2fsp\_translation\_info");
\end{shaded}

toma el archivo \textit{mapping} generado anteriormente y retorna un elemento que contiene todas las nomenclaturas correspondientes según el elemento utilizado.

\begin{shaded}
t\_info.fwla\_to\_fsp(String element);
\end{shaded}

Éste último servicio realiza la traducción y retorna el nombre del elemento correcto. La traducción de los nombres está dada por el siguiente método:


\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white}
\lstset{
	frame=lrb,
	xleftmargin=\fboxsep,
	xrightmargin=-\fboxsep,
	language=java,
	showstringspaces=false,
	keywordstyle=\color{blue},
	morekeywords={private,String,return},
	tabsize=2,
	basicstyle=\ttfamily\scriptsize,
}
\begin{lstlisting}[caption=Invocación de \textit{yawl2fsp}]
private String replaceFLWANames(String propertyFLWA){
	if(propertyFLWA.length()>0){
		for(int i=0; i<vectorTask.size();i++){
			propertyFLWA = propertyFLWA.replaceAll(vectorTask.get(i).getId()+".start",
		  t_info.fwla_to_fsp(vectorTask.get(i).getId()+".start"));
			propertyFLWA = propertyFLWA.replaceAll(vectorTask.get(i).getId()+".end",
		  t_info.fwla_to_fsp(vectorTask.get(i).getId()+".end"));
		}
	}
	return propertyFLWA;
}
\end{lstlisting}
Aquí se realiza la traducción de los nombres de los modelos a los correspondientes en la especificación generada. El valor a reemplazar se obtiene por un servició otorgado de la librería \textit{yawl2fsp} el cual permite la traducción correcta de los elementos utilizados.\\ Luego de la traducción de los elementos se realiza la traducción de los operadores ya que éstos, como se explico en la sección anterior, fueron representados de manera diferente con el objetivo de facilitar su escritura. El proceso de traducción es similar a lo realizado en las propiedades otorgadas por las plantillas. Por último para poder terminar el proceso de reconstrucción de la especificación antes de ser verificadas, se construyen los fluentes y se crean las aserciones, éstas últimas representaran las propiedades definidas.\\\newline
Para la incorporación de los fluentes en la especificación, como se dijo anteriormente, se expresan en \emph{FLTL} y el proceso de traducción es similar a los anteriores.

\subsection{Model checker \textit{LTSA}}
La verificación de propiedades se realiza mediante la técnica de model checking, específicamente, en este trabajo, mediante el \textit{Labelled Transition System Analyser} (LTSA). \emph{LTSA} recibe la especificación generada a través de \textit{yawl2fsp} y \emph{FLWA}, y su resultado, verificación exitosa o contra-ejemplo, es nuevamente procesada por \emph{FLWA} para su presentación al usuario en términos del workflow analizado. \\\newline
\emph{LTSA} como se detalló en el capítulo 3, no es una herramienta que pueda ser ejecutada desde linea de comando como es el caso de \textit{yawl2fsp}. Como consecuencia a esto, se tubo que recurrir al uso del código fuente de \emph{LTSA} y se lo agrego al código desarrollado de \emph{FLWA}, es decir que \emph{LTSA} está incluido en \emph{FLWA}. Para lograr este propósito se realizó una serie de modificaciones a la herramientas \emph{LTSA}. Se definió una estructura \textit{LTSA} que brinde los servicios suficientes para la compilación y verificación de propiedades. Estos servicios se mencionan a continuación.

\begin{shaded}
public void parse(){...}
\end{shaded}

Este servicio definido permite hacer la llamada a las librerías de LTSA para la \textit{parsear} cada uno de los elementos del \emph{FSP} recibido. Cualquier inconveniente se detecta en este proceso y en un módulo separado donde se compilan las aserciones definidas por la posibilidad de algún error se sintaxis. Estos errores son presentados al usuario en forma de notificaciones.

\begin{shaded}
public void compileAll(){...}
\end{shaded}

Es el método encargado de compilar cada uno de los procesos definidos. Esta compilación es necesaria posteriormente para definir los procesos en los cuales se va querer aplicar las propiedades que sido elegidas para ser verificadas.

\begin{shaded}
public String[] getDefinitionArray(){...}
\end{shaded}

\begin{shaded}
public CompositeState runDefinition(String assertDefinition, LTSOutput output){...}
\end{shaded}

El primer método determina las propiedades elegidas y el en segundo publica el servicio desarrollado que permite verificar una propiedad determinada y permite obtener el resultado de esta operación en una cadena que va ser manipulada para la observación del resultado. Este método se utiliza una vez que la compilación de la especificación haya sido exitosa. Las propiedades serán ejecutadas una a una dependiendo de la selección del usuario. El uso del segundo parámetro se realiza para mostrar en una pantalla adicional las propiedades elegidas y el resultado de éstas para el proceso elegido.
LTSOutput es una interfaz que permite arrojar ciertos resultados siempre y cuando sean implementados los métodos para la visualización de los mismos.\\\newline

Si la compilación de la especificación del modelo y las propiedades ha sido satisfactoria, las mismas son presentadas en forma de botones en una nueva ventana junto a los procesos y estos últimos también pueden ser elegidos. Los resultados como se menciono en el capítulo anterior, son procesados cada vez que se elije alguna de las propiedades y son visualizados en un campo de texto.\\

\subsection{Resultados de verificación de propiedades}
Durante éstas últimas secciones se ha detallado el proceso de traducción y verificación de las propiedades definidas sobre el modelo. Sin embargo, es necesario representar los resultados de las verificaciones al usuario. A continuación se presentan algunos de los detalles para lograr las trazas y los resultados de los mismos.\\\newline

Para la descripción de estos resultados, se considera que para los casos en que la propiedad es validad logicamente no se obtiene contra-ejemplos o una traza que la haga invalida. De este modo solo se representa el resultado de ésta coloreando la propiedad de color verde. En caso de que la propiedad sea invalida, el escenario es diferente y cuyo resultado de \emph{LTSA} se obtiene una traza de ejecución de eventos que la hace invalida. Utilizando los siguientes servicios se puede comunicar la traza que se desea representar con el modelo de la pantalla inicial.

\begin{shaded}
public void setTrace(Object[] traceStateList);
\end{shaded}

\begin{shaded}
public Object[] getTrace();
\end{shaded}

Las trazas están compuestas de las tarea y condiciones que se encuentra en el resultado arrojado por \emph{LTSA}. \emph{LTSA} arroja los eventos y estos últimos tienen que ser traducidos nuevamente a los nombres originales, de los cuales se obtiene las tareas y condiciones antes mencionados. Para el tratado de las flechas se hace un proceso de conjuntos de manera de tener las correctas(pertenezcan a la traza).\\

Todo este proceso es necesario para poder visualizar las trazas en el modelo principal con el objetivo de poder facilitar el análisis de los resultados por \emph{LTSA}. De manera que se pretende que el usuario pueda volver a verificar una nueva propiedad, en cuyo caso el modelo volverá a su estado inicial y la traza de ejecución desaparecerá.


